Deadlock-freeness with probability

Given P() as a process, the following assertion asks the (min/max/both) probability that P() is deadlock-free or not.

#assert P() deadlockfree with pmin/ pmax/ prob;

Reachability with probability

Given P() as a process, the following assertion asks the (min/max/both) probability that P() can reach a state at which some given condition is satisfied.

#assert P() reaches cond with prob/ pmin/ pmax;

Linear Temporal Logic (LTL) with probability

In PAT, we support the full set of LTL syntax. Given a process P(), the following assertion asks the (min/max/both) probability that P() satisfies the LTL formula.

#assert P() |= F with prob/ pmin/ pmax;

where F is an LTL formula.

Refinement Checking with probability

PAT now also supports refinement checking in PCSP. User could define a non-probabilistic property using CSP# as a specificaiton. Then PAT could calculate the probability that the system behaves under the constraint of the specification.

          #assert P() refines Spec() with prob/ pmin/ pmax;

where Spec() is the user-defined specification.

The precision of the probability can be changed in the system configurations.